enrich
   intlista, 
   int-gcd

with
   

   
   
   functions  all_prime_divisors : int → intlist;
             comment: canonical prime factorization of n, e.g. 12 = 2 * 2 * 3;
              Σ . : intlist → int;
              Π . : intlist → int;
              max : intlist → int;
              min : intlist → int;
              count-i2j : int × int → intlist;
             comment: count-i2j(i, j) = [i, i+1, ..., j];
              countFun : int × int × (int → int) → intlist;
              mapFun : (int → int) × intlist → intlist;
              filterFun : (int → bool) × intlist → intlist;
             comment: keep all elements with test true, remove others.;
              coprimes : int → intlist;
             comment: for i, the list of integers j with gcd(i, j) = 1 and 1 ≤ j ≤ i.;
              euler-phi : int → int;
             comment: Euler's phi function, also known as Euler's totient function, length of coprimes(i).
	                                  It gives the order of the multiplicative group of integers modulo n 
	                                  (the group of units of the ring Z/nZ).;
   predicates  primes : intlist;
              comment: true if all ints in the list are primes.;
   
   variables  intfun : int → int;
              intboolfun : int → bool;
   
   

   

   axioms sum-empty :  ⊦ Σ [] = 0;
          used for: s, ls;
          sum-rec :  ⊦ Σ(i ' + ints) = i + Σ ints;
          used for: s, ls;
          prod-empty :  ⊦ Π [] = 1;
          used for: s, ls;
          prod-rec :  ⊦ Π(i ' + ints) = i * Π ints;
          used for: s, ls;
          max-empty :  ⊦ max([]) = 0;
          used for: s, ls;
          max-def :  ⊦ ints ≠ [] → max(ints) ∈ ints ∧ (∀ i. i ∈ ints → i ≤ max(ints));
          min-empty :  ⊦ min([]) = 0;
          used for: s, ls;
          min-def :  ⊦ ints ≠ [] → min(ints) ∈ ints ∧ (∀ i. i ∈ ints → min(ints) ≤ i);
          primes-def :  ⊦ primes(ints) ↔ (∀ i. i ∈ ints → prime(i));
          all_prime_divisors-base :  ⊦ i < 2 → all_prime_divisors(i) = [];
          used for: s, ls;
          all_prime_divisors-prime :  ⊦ prime(i) → all_prime_divisors(i) = i ';
          used for: s, ls;
          all_prime_divisors-rec
          :  ⊦ 2 ≤ i ∧ ¬ prime(i) → all_prime_divisors(i) = all_prime_divisors(i / max_prime_divisor(i)) + max_prime_divisor(i) ';
          coprimes-def :  ⊦ coprimes(i) = filterFun(λ j. gcd(i, j) = 1, count-i2j(1, i));
          euler-phi-def :  ⊦ euler-phi(i) = n→i(# coprimes(i));
          counti2j-empty :  ⊦ j < i → count-i2j(i, j) = [];
          used for: s, ls;
          counti2j-rec :  ⊦ i ≤ j → count-i2j(i, j) = count-i2j(i, j - 1) + j;
          countFun-base :  ⊦ j < i → countFun(i, j, intfun) = [];
          countFun-rec :  ⊦ i ≤ j → countFun(i, j, intfun) = intfun(i) ' + countFun(i + 1, j, intfun);
          mapFun-base :  ⊦ mapFun(intfun, []) = [];
          used for: s, ls;
          mapFun-rec :  ⊦ mapFun(intfun, i ' + ints) = intfun(i) ' + mapFun(intfun, ints);
          used for: s, ls;
          filterFun-base :  ⊦ filterFun(intboolfun, []) = [];
          used for: s, ls;
          filterFun-keep :  ⊦ intboolfun(i) → filterFun(intboolfun, i ' + ints) = i ' + filterFun(intboolfun, ints);
          used for: s, ls;
          filterFun-remove :  ⊦ ¬ intboolfun(i) → filterFun(intboolfun, i ' + ints) = filterFun(intboolfun, ints);
          used for: s, ls;

   

   
end enrich